RecordUpdatePreservesType.agda:18,14-17
R !=< Q
when checking that the expression old has type Q
